Rosetta Lisp in Idris

Rosetta LispのIdris実装について。

Idris。依存型を搭載したプログラミング言語を触ってみたくやってみた。

基本的な構文などはHaskellによく似ているが、型システムの感覚的な距離は、OCamlとHaskellよりもHaskellとIdrisのほうがずっと離れている。Type-Driven Development with IdrisというIdrisの開発者によって書かれた本があり、 1. OVERVIEW を無料で読むことができるので、依存型を搭載したプログラミング言語の「見た目」を知りたければまずこれを読むのが良いだろう。

以下、おおよそHaskellの視点でIdrisの特徴について記載しているが、依存型を持つプログラミング言語は非常に少なく、Idris以外は触れたことも無いので、取り上げた特徴が依存型を持つ言語全体で特有のものなのかIdrisの言語デザイン特有のものなのかの区別を付けていない。そのうち補足できたら補足したい。

まず実際に書いてみてぶち当たるのがTotality checkerだ。Totality checkerは関数が入力に対して必ず有限な時間で停止することを検査するが、Totality checkerがtotalと判定できるものは思っていたよりも保守的という感覚を覚える。これは(比較できる対象ではないが)NLL以前のRustのような、思っていたよりも型システムを説得するのが大変、という感覚。

依存型を用いたプログラミング。Idrlispのビルトイン関数の実装では、入力の値の引数リストとシグネチャでパターンマッチを行い、そのパターンに対応するデータを処理したりするが、これをごく普通に型を計算する関数として表現できる。さらにその関数を用いて引数のシグネチャに適合するマッチした結果を返す関数といったような表現を行える。

code:Signature.idr.hs

-- S式を表現するデータ型

data Sexp

= SNum Double

| SStr String

| ...

-- シグネチャを表現するデータ型

public export

data Signature

= Num

| Str

| ...

-- シグネチャにS式をマッチした結果、を計算する関数を定義できる

SignatureType : Signature -> Type

SignatureType Num = Double

SignatureType Str = String

...

-- シグネチャにS式をマッチする実装

-- 引数の値 sig に依存した型 SignatureType sig が含まれる

match : (sig : Signature) -> Sexp -> Either String (SignatureType sig)

match Num (SNum n) = Right n

match Num _ = Left "Expected Num"

match Str (SStr s) = Right s

match Str _ = Left "Expected Str"

...

普通に便利に使えるなあという感じ。実際の利用例はIdrlib.idrなどを参照。他にも、例えばHaskellで type Hoge = Int とするような型エイリアスの定義もIdrisでは単に関数で定義される。こういう発想の違いが随所に見られて新鮮さがある。

code:Alias.idr.hs

public export

Value : Type

Value = Sexp Native

一方、他にもTDD with Idrisでは色々「依存型があることでどう異なるか、どう表現するか、どう実践するか」が解説されており、それは楽しく読めたのだけれど、Idrlispではイマイチ活かし切れなかったかなとも。

Idrlispの実装中一番なるほどなあと感心したのはcontribパッケージに付属しているパーサコンビネータで、この実装ではパーサの型 Grammar がパース成功時に必ず何らかの入力を消費するかを型レベルの Bool 値でトラックしている。これによって many のようなコンビネータには成功時には必ず入力を消費するパーサのみ与えられるようになっていたり、入力を消費するということはすなわち必ず入力が尽きるということでtotality checkerによってパース処理が停止することが保証できたりしている。

その他色々。Idrisは名前のオーバーロードを多用する。 do 記法は完全なシンタックスシュガー (GHCの RebindableSyntax 相当) であるし、ユーザー定義のデータ型、例えば上の Sexp でも (::) Nil を定義することで平然と [Num 1, Num 2, Num 3] と記述できる。これは当然、型チェックに失敗したときのエラーが非常にわかりづらくなる。しかし依存型がある故に型クラスで表現するような一般化を与えるのも難しい場合が多いのでどうすればいいかというと何とも...

コンパイルはとてつもなく遅い。主要因は型チェックだろう。